T:Type, P:(Tprop{i:l}). l_exists([]; T; x.P(x))  False 

latex

Definitions	t  T, P  Q, P  Q, P  Q, x:A. B(x), x(s), l_exists(L; T; x.P(x)), P  Q, prop{i:l}, x:A. B(x), False
Lemmas	false wf, l member wf, nil member